COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\\M0BDR25\M1BDI25\M2NGR30\M3XMAS25\M4NGB25\M5NGR40\.
C00008 ENDMK
C⊗;
\\M0BDR25;\M1BDI25;\M2NGR30;\M3XMAS25;\M4NGB25;\M5NGR40;\.
\F5\CARTIFICIAL INTELLIGENCE LABORATORY
\CCOMPUTER SCIENCE DEPARTMENT
\CSTANFORD UNIVERSITY
\CSTANFORD, CALIFORNIA 94305
\F0





							June 18, 1974





Professor Garrett Birkhoff
Department of Mathematics
Harvard University
Science Center
One Oxford Street
Cambridge, Massachusetts 02138

Dear Garrett:

\J	Sorry I didn't get around to looking at your article until now, and
I hope these comments are still of some use to you.

	In general, I shall leave artificial intelligence to Marvin Minsky
even though his point of view and mine are not quite identical.  Enclosed,
however, is a review of the \F1Lighthill Report\F0 that will appear in
the journal \F1Artificial Intelligence\F0.  Some of the ideas there expressed
may be relevant to your purposes.

	From my point of view, the main omission in your article is any
discussion of the computer program as an object of mathematical study.
Since the properties of a computer program are mathematical consequences
of its structure, it is a continuing mathematical disgrace that the best
way to get a program right is to try it out on test cases, make corrections
suggested by the errors found, and continue this process until you can't
think of any more cases to try.  Then the next person who gets the program
almost immediately finds additional bugs.  Any mathematician should want
to prove that the program meets its specifications.  Moreover, the notion
of formal mathematical proof includes the property that proofs can be
checked by computer even if they can't easily be generated by computer.

	I started this line of research around 1960, and since 1965 it has
become increasingly active, and important contributions have been made
by Robert Floyd, Dana Scott, Tony Hoare, Zohar Manna and many others.
I ccnsider the formalization of properties of computer programs and
their proof in suitable axiomatic systems to be the mathematical core
of computer science.  The properties considered include termination,
mathematical relations between input and output, equivalence of programs,
the correctness of compilers, i.e. that the object program carries out
the computation described by the source program.  In support of this goal
proof checking programs have been written, axiomatizations of the properties
of programs have been developed, and theorems have been proved that allow
the correctness of a program to be reduced to truth of a sentence in
predicate calculus.

	In all this it is necessary to distinguish the \F1theory of computation\F0
in which the correctness of particular programs is studied from the
\F1theory of computability\F0 which is concerned with whether a given
class of problems can be solved at all by computer.

	Don Knuth's letter gives several examples from what is called
applied complexity theory, i.e. a theory that determines upper and
lower bounds to the amount of computation required to solve a problem.
However, I think the subject deserves systematic recognition in any
general discussion of the relations between mathematics and computer
science.

	I hope these remarks will be of some help.\.


						
							Sincerely yours,
			


							John McCarthy
							Professor of Computer Science
							Director, Artificial Intelligence Laboratory